This invention relates to design and synthesis of digital circuits.
Hardware description languages (HDLs) have been used for some time to design electronic circuits, and in particular to design synchronous (clocked) digital circuits. One class of hardware description languages are xe2x80x9cregister-transfer languagesxe2x80x9d (RTLs) in which the circuit has, or is abstracted to have, a set of registers, and the language specifies the values of the registers in each clock period in terms of the values in the previous clock period. A widely used HDL is Verilog, which has been standardized as IEEE standard 1364-1995, and for which numerous software tools are available. Verilog supports a variety of specification approaches, including a RTL approach.
Design of complex digital circuits, such as pipelined and superscalar processors, using an RTL approach requires a hardware architect to specify the overall functionality of the system which can be defined in terms of modular components that are defined separately, as well as specify the correct coordination of concurrent processing modules in the circuit. As hardware systems become more complex, for example pipelined processors which allow out-of-order and speculative instruction execution, this task is increasingly time consuming and is subject to human error.
Other HDL approaches attempt to specify a digital circuit in xe2x80x9cbehavioralxe2x80x9d terms, without necessarily identifying the structure of the underlying circuit. For instance, Verilog supports such a behavioral specification approach. However, it is not always possible or feasible to synthesize an equivalent digital circuit from such a behavioral specification.
A variety of software tools are available for processing HDL specifications, including tools for simulating the specified circuits. Formal verification of the correctness of an HDL specification is often difficult, or even impossible, due in part to the nature and complexity of the specification.
In a general aspect, the invention is a method of specifying and synthesizing a synchronous digital circuit by first accepting a specification of an asynchronous system in which stored values are updated according to a set of state transition rules. For instance, the state transition rules are specified as a Term Rewriting System (TRS) in which each rule specifies a number of allowable state transitions, and includes a logical precondition on the stored values and a functional specification of the stored values after a state transition in terms of the stored values prior to the state transition. The specification of the asynchronous circuit is converted into a specification of an synchronous circuit in which a number of state transitions can occur during each clock period. The method includes identifying sets of state transitions, for example by identifying sets of TRS rules, that can occur during a single clocking period and forming the specification of the synchronous circuit to allow any of the state transitions in a single set to occur during any particular clocking period.
In one aspect, in general, the invention is a method for determining a specification a synchronous digital circuit. The method includes accepting a first specification of a first asynchronous digital system, including accepting a specification of multiple data elements whose values define the state of the system and a first set of state transition rules for the asynchronous digital system. The method then includes determining a specification of a synchronous digital circuit from the specification of the asynchronous digital system, such that during at least some clocking periods the synchronous digital circuit makes a state transition equivalent to state transitions specified by multiple the state transition rules specified for the asynchronous digital system.
The method can include one or more of the following features:
Each state transition rule includes a specification of a precondition that must be satisfied by the state of the system to apply the state transition rule, and a specification of a resulting state that is reached as a result of applying the state transition rule. For instance, the state transition rules are defined as a term rewriting system, and the specification of the synchronous digital system is in a register transfer language.
The method further includes scheduling the state transition rules by identifying one or more sets of conflicting state transition rules. State transitions specified by different rules in one of the conflicting sets may conflict in their access to data elements of the system.
Determining the specification of the synchronous system includes determining the specification such that during any clocking period, the synchronous digital circuit makes states transitions equivalent to at most one state transition rule from each conflicting set of state transition rules.
Determining the specification of the synchronous system includes determining a specification of arbitration logic associated with each conflicting set of state transition rules such that the arbitration logic generates trigger signals that allow at most one state transition rule from the conflicting set of states to be applied in a single clocking period. For instance, the arbitration logic includes a round-robin priority encoder for generating the trigger signals.
The method further includes determining a specification of arbitration logic that generates trigger signals for sets of state transitions rules such that the rules in each of said are applicable in at least some order to the asynchronous digital system.
The method further includes transforming the first specification of the first asynchronous digital system into a second specification of a second asynchronous digital system. The second specification includes a second set of state transition rules, and the second asynchronous digital system includes pipeline. At least some of the first state transitions rules each correspond to multiple of the second state transition rules such that each of these corresponding rules is associated with a different stage of the pipeline.
The method includes adding a number of composite rules to the first specification, wherein each composite rule is associate with multiple of the first state transition rules, and each state transition specified by one of the composite state transition rules is equivalent to a sequence of state transitions each specified by the first set of state transition rules.
Accepting the specification of the data elements further includes accepting a specification of an abstract data type, such as a first-in-first-out queue, and wherein determining a specification of a synchronous digital circuit includes determining an implementation of the abstract data type.
The synchronous digital circuit can implement a computer processor, and state transitions of the asynchronous digital system are associated with changes in values stored in storage elements of the computer processor.
Determining the specification of the synchronous circuit further includes determining a preliminary specification of a digital circuit, and optimizing the preliminary specification a correspondence between the preliminary specification and the specification of the asynchronous digital system.
Aspect of the invention may include one or more of the following advantages:
The approach embodied in the invention allows a hardware architect to develop a specification of an asynchronous system as an initial step to developing a synchronous circuit specification. Specification of the asynchronous system is typically simpler than direct specification of a corresponding synchronous system in part because the architect is relieved of the task of scheduling concurrent operations during clock periods. Furthermore, by not having to deal in low-level implementation tasks, there is less chance of human error.
Use of a Term Rewriting System (TRS) provides a basis for formal verification of system specifications. Furthermore, the TRS provides a basis for automated or semi-automated transformations of a specification, for example, to introduce pipelined or superscalar aspects into the circuit specification.
Use of abstract data types, such as FIFOs or content-addressable memory, also relieves the hardware architect from issues related to low-level design. A circuit realization of an abstract data type can be deferred until later in the design process.
Maintaining a relationship or mapping between a synchronous circuit specification and the initial asynchronous circuit specification simplifies optimization of the synchronous circuit.
The approach can be used to interface to previously designed synchronous modules. In this way, a hardware architect can concentrate on the coordination and interconnection of these predefined modules without having to redesign the modules themselves.
The approach can also be used to design synchronous modules that are then used in other circuit design approaches.
Other features and advantages of the invention are apparent from the following description, and from the claims.